Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Final borrow #912

Merged
merged 17 commits into from
Jan 29, 2024
Merged

Final borrow #912

merged 17 commits into from
Jan 29, 2024

Conversation

arnaudgolfouse
Copy link
Collaborator

Experiment to repair proofs when using a third field in mutable borrows.

In short, in the following code:

let mut x = 0i32;
let mut y = 0i32;
let ref_x_1 = &mut x;
let ref_x_2 = &mut *ref_x_1;
let ref_y_1 = &mut y;
let ref_y_2 = &mut *ref_y_1;

// ref_x_1 is never used here

let z = *ref_y_1;

Then:

  • The third field of ref_x_1 and ref_x_2 should be the same, because ref_x_1 is "dead" after the reborrow (we say that this reborrow is final)
  • This is not the case for ref_y_1, so the third field of ref_y_1 and ref_y_2 is not the same.

@arnaudgolfouse arnaudgolfouse force-pushed the final-borrow branch 6 times, most recently from 7de8c30 to 90034f1 Compare December 11, 2023 16:32
@arnaudgolfouse
Copy link
Collaborator Author

Some tests had their source (.rs) changed:

  • iterators/02_iter_mut:

    • in completed: self.resolve() becomes (*self).inner@ == (^self).inner@
    • in produces, rather than comparing the two sequences directly, we need to compare each borrow by their current/final value.

  • iterators/06_map_precond: remove let _ = self;

  • take_first_mut: replace ^self == *self with (*^self_)@.len() == 0 && (^*self_)@.len() == 0

    We cannot prove ^self == *self, because we used std::mem::take, and the new borrow may not have the same id.

@jhjourdan
Copy link
Collaborator

Good !

First, CI is failing, which is indicating some of the sessions need to be updated. And indeed, it says that the iter_mut session is obsolete. Could you please update it?

in completed: self.resolve() becomes (*self).inner@ == (^self).inner@

This is suspicious. Why is this necessary? It should be equivalent, right?

iterators/06_map_precond: remove let _ = self;

I confirm that this is OK. This dates from the time where we had an assertion that we needed to prove the invariant. This assertion disappeared, so we can remove this hack.

That being being said, this is a real problem: we may need a way to reliably delay resolution without breaking final reborrows...

@xldenis
Copy link
Collaborator

xldenis commented Dec 12, 2023

That being being said, this is a real problem: we may need a way to reliably delay resolution without breaking final reborrows...

Let's not complicate an already complicated change with hypothetical edge-cases. The day when this becomes necessary we can revisit it.

@xldenis
Copy link
Collaborator

xldenis commented Dec 12, 2023

This is suspicious. Why is this necessary? It should be equivalent, right?

That's really weird, if this is breaking it also would indicate deeper issues to me. since ^self = *self should imply that.

@jhjourdan
Copy link
Collaborator

Let's not complicate an already complicated change with hypothetical edge-cases. The day when this becomes necessary we can revisit it.

Yes, of course! I was mentioning this simply because we may need to do something at some point.

@jhjourdan jhjourdan marked this pull request as ready for review December 12, 2023 17:07
jhjourdan
jhjourdan previously requested changes Dec 13, 2023
View reviewed changes
Copy link
Collaborator

@jhjourdan jhjourdan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All in all I think this is very good news and should be merged quickly. Thanks.

There are still quite a few changes needed. Namely:

  • First, I think there are a few bugs which I detailed in the review.
  • Cleanup sessions. A few sessions contains "timeout" entries for some provers. They should not be included for successful goals (Why3 shows a warning for them, I think)
  • The iter_mut test has an obsolete session. The new shapes file should be comitted.
  • Some session files contains duplicate provers used for the same goals. This is not really a problem here, but it slows down the CI, so you should be cautious about them, and identify what part of your workflow with Why3IDE makes these duplicated prover calls.
  • Not all changes to iter_mut and take_first_mut have been propagated to creusot_contracts.
  • @xldenis have merged Allow logically reborrowing through derefs of ghost and indexing things #852, so you should resolve the conflicts, and add reborrowing of indexed projections

I'm sorry to ask you these changes, but you're almost there!

creusot-contracts/src/std/slice.rs Outdated Show resolved Hide resolved
creusot-contracts/src/std/slice.rs Outdated Show resolved Hide resolved
creusot/src/backend/program.rs Outdated Show resolved Hide resolved
creusot/src/backend/program.rs Show resolved Hide resolved
creusot/src/backend/place.rs Outdated Show resolved Hide resolved
creusot/src/analysis/not_final_places.rs Outdated Show resolved Hide resolved
creusot/src/analysis/not_final_places.rs Show resolved Hide resolved
creusot/src/analysis/not_final_places.rs Outdated Show resolved Hide resolved
creusot/src/analysis/not_final_places.rs Outdated Show resolved Hide resolved
creusot/src/analysis/not_final_places.rs Outdated Show resolved Hide resolved
@jhjourdan
Copy link
Collaborator

That's really weird, if this is breaking it also would indicate deeper issues to me. since ^self = *self should imply that.

Actually it does not imply this, because @arnaudgolfouse's version does not say anything about the inner tag. And I think @arnaudgolfouse is right: his change is necessary because of the change of the specification of take_first_mut.

That being said, (^self).inner@ == Seq::EMPTY would have been clearer (same remark for take_first_mut, BTW).

@arnaudgolfouse arnaudgolfouse force-pushed the final-borrow branch 4 times, most recently from 1ecf9ed to 4678ee2 Compare December 20, 2023 09:59
@arnaudgolfouse arnaudgolfouse force-pushed the final-borrow branch 2 times, most recently from fc85e96 to d5333ab Compare January 22, 2024 12:20
@arnaudgolfouse
Make borrows non extensible
8a37de4
@arnaudgolfouse
Get back to concrete current/final fields, with an addr field
e70ae74 
This is functionally the same, but it helps why3 to detect that the `final` field does not change on reborrows.
@arnaudgolfouse
Remove the make_new_addr call on reborrows
5cf2f2d 
This is not necessary, because a reborrow `y = &mut *x` is translated as
```
y <- Borrow.borrow_mut (* x)
x <- { x with current = (^ y) }
```
And `Borrow.borrow_mut` already creates a fresh address.
@arnaudgolfouse
Copy link
Collaborator Author

This should be good to go

@jhjourdan
Copy link
Collaborator

Could you please do a pass on each of my comments, check you have indeed handle them, and mark them as resolved? Thanks !

@arnaudgolfouse arnaudgolfouse merged commit 846d296 into creusot-rs:master Jan 29, 2024
4 checks passed
This was referenced Feb 21, 2024
Closed
Closed
Closed
Draft
@arnaudgolfouse arnaudgolfouse deleted the final-borrow branch February 23, 2024 09:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jhjourdan jhjourdan jhjourdan left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@arnaudgolfouse @jhjourdan @xldenis